$\forall$$M$:MsgA, $k$:Knd, $l$:IdLnk. $M$.bframe($k$ sends on $l$) $\in$ Prop